Nuprl Lemma : first0
11,40
postcript
pdf
L
:(Top List). firstn(0;
L
) ~ []
latex
Definitions
x
:
A
.
B
(
x
)
,
firstn(
n
;
as
)
,
Y
,
if
b
then
t
else
f
fi
,
i
<z
j
,
ff
,
t
T
Lemmas
top
wf
origin
L:(Top List). firstn(0;L) ~ [] L:(Top List). firstn(0;L) ~ [] x:A. B(x)
T